#ifndef Minisat_Proof_ITP_H
#define Minisat_Proof_ITP_H

#include "Proof.h"
#include "Solver.h"
#include "base/aig.h"
#include <vec.h>
#include <vector>

namespace MinisatProof
{


// Interpolation interface definition

/**
@brief ITP is a ProofTraverser  
*/
class ITP : virtual public ProofTraverser 
{

public:
   ITP():_camp(256,0){} // 0 is local to B 
   static const AigLit VarA = -1 ;
   static const AigLit VarB = -2 ; 

protected:
   ::vec<AigLit>   _subITP; ///< sub interpolant the index follow the leant clause
   bool            _inv;    ///< the interpolant is the inverse or not 

public:
   ::vec<AigLit>        _base; ///< The literal is Local A or B or Base with AigLit 
   std::vector<bool>    _camp;
};

/**
@brief Boolean operation pure interface 
*/
class AigCal
{
public:
    virtual ~AigCal(){};
    virtual AigLit AND( const AigLit & a , const AigLit & b)= 0 ;
    virtual AigLit OR( const AigLit & a , const AigLit & b){ return inv( AND ( inv(a) , inv(b)) );}
    virtual AigLit ITE(const AigLit & c , const AigLit & t , const AigLit & f){ return OR( AND(c,t),AND(inv(c),f)) ; }
};

class InterpolantITP : virtual public ProofTraverser 
{
public :
   virtual AigLit  interpolant() =0 ; 
};


/**
@brief Pudlark construction method
*/
class PITP : virtual public ITP , virtual public AigCal , virtual public ProofTraverser 
{
public:
   PITP():ITP(){}
   virtual ~PITP(){}

   virtual void root(const vec<Lit> &  c , uint8_t A);
   virtual void chain(const vec<ClauseId> & cs , const vec<Lit> & xs );
private:
   AigLit resolve(AigLit a ,Lit v,  AigLit b);

};

/**
@brief McMillian Construction Algorithm
ROOT: 
(A) conjuction of global literal (B) const 1 
LEANT (a) OR (b) AND (g) AND
*/
class MITP : virtual public ITP , virtual public AigCal , virtual public ProofTraverser 
{
public:
   MITP(uint8_t inv) :ITP(),_inv(inv){}
   virtual ~MITP(){}

   virtual void root( const vec<Lit> & c , uint8_t A);
   virtual void chain( const vec<ClauseId> & cs , const vec<Lit> & xs);
private:
   AigLit  resolve( AigLit a, Lit v , AigLit b );
protected:
   uint8_t _inv;
};


/**
@brief Structural Hashed Interpolant ( implementation of AigCal by Strash ) 
*/
class SITP : virtual public ITP , virtual public AigCal , virtual public InterpolantITP 
{
    StrashAIG & _ref;
protected:
    AigLit      _interpolant;
public:
    //--- construct & destruct ---
    SITP( StrashAIG & s):_ref(s){}
    virtual ~SITP(){}
    virtual AigLit AND( const AigLit & a , const AigLit & b){return _ref.createAND( a, b);}
    virtual AigLit interpolant(){return _interpolant;}
};

/**
@brief Constructing mutltiple interpolant ON_THE_FLY
*/
class MultiSITP : virtual public ProofTraverser 
{
public :
    ::vec<SITP  *> _sitp;
   //--- construct & destruct 
    MultiSITP( unsigned a );
    virtual ~MultiSITP();
    void set( unsigned i , SITP * s ){ _sitp[i] = s ;}

    SITP & operator[]( unsigned i ){ return * (_sitp[i] ); }

    //--- concrete func of ProofTraverser --- 
    virtual void root   (const vec<Lit>& c , uint8_t A);
    virtual void chain  (const vec<ClauseId>& cs, const vec<Lit>& xs);
    virtual void deleted(ClauseId c);
    virtual void done   ();
};


class SMITP : virtual public SITP , virtual public MITP
{
public:
    virtual ~SMITP(){}
    SMITP( StrashAIG & k , uint8_t p ):SITP(k),MITP(p){}
    void done(){ _interpolant = _inv?(inv(_subITP.last())):_subITP.last(); }
    void done( unsigned id , const vec<Lit> & c );
};

class SPITP: virtual public SITP , virtual public PITP
{
public:
    virtual ~SPITP(){}
    SPITP( StrashAIG & k ):SITP(k){}
    void done(){ _interpolant = _subITP.last(); }
    void done( unsigned id , const vec<Lit> & c );
};

struct Checker : virtual public ProofTraverser 
{
    vec< vec<Lit> >         clauses;
    vec< vec< ClauseId > >  vcs;
    vec< vec<Lit> >         vxs;
    vec< uint8_t >          phase; // 0 A 1 B 3 Chain
    
    int TRA_INT;
    bool _resolve_check;

    Checker( bool r):TRA_INT(0),_resolve_check(r){}
    void root   (const vec<Lit>& c , uint8_t A);
    void chain  (const vec<ClauseId>& cs, const vec<Lit>& xs) ;
    void deleted(ClauseId c) ;
    void resolve(vec<Lit>& main , Lit l, vec<Lit>& other);
    void traverse( ProofTraverser & ); 
    void done();
};

class ITPMgr
{
   protected:

   ProofTraverser * _pft; // internal  
   SITP           * _itp; // construction 
   Proof          * _pf;  // proof 
   AigLit           _interpolant; // constructed 

   public:
      
   enum CONST_MODE{ ON_THE_FLY , NONE , HDD , MEM } MODE;
   enum ALGORITHM { PUDLARK , MCMILLIAN }           ITP;
   
   int ITP_PHASE;
   int CC_MIN;// 
   
   ITPMgr( ):
      _pft( NULL ), _itp( NULL ),_pf( NULL ),
      MODE( ON_THE_FLY ),ITP(PUDLARK),
      ITP_PHASE(1),CC_MIN(1)
      {}
   ~ITPMgr();

   ProofTraverser * init( Solver & S, StrashAIG & ckt ); // parameter for _itp 
   AigLit           itpGen();
};

};// NAMESPACE MINISAT_PROOF
#endif
